|
|
Statická analýza v nástroji Facebook Infer zaměřená na detekci porušení atomičnosti
Harmim, Dominik ; Smrčka, Aleš (oponent) ; Vojnar, Tomáš (vedoucí práce)
Cílem této práce je navrhnout statický analyzátor, který bude sloužit pro detekci porušení atomicity. Navržený analyzátor Atomer je implementován jako modul pro Facebook Infer, což je volně šířený a snadno rozšířitelný nástroj, který umožňuje efektivní modulární a inkrementální analýzu. Analyzátor pracuje na úrovni sekvencí volání funkcí. Navržené řešení je založeno na předpokladu, že sekvence, které jsou zavolány atomicky jednou, by měly být pravděpodobně volány atomicky vždy. Implementovaný analyzátor byl úspěšně ověřen a vyhodnocen jak na malých programech, vytvořených pro testovací účely, tak na veřejně dostupných testovacích programech, které vznikly ze skutečných nízkoúrovňových programů.
|
|
|
Advanced Static Analysis of Atomicity in Concurrent Programs through Facebook Infer
Harmim, Dominik ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
Atomer is a static analyser based on the idea that if some sequences of functions of a multi-threaded program are executed under locks in some runs, likely, they are always intended to execute atomically. Atomer thus strives to look for such sequences and then detects for which of them the atomicity may be broken in some other program runs. The author of this master's thesis proposed and implemented the first version of Atomer as a plugin of the Facebook Infer framework in his bachelor's thesis. In the master's thesis, a new and significantly improved version of Atomer is proposed. The improvements aim at both increasing scalability as well as precision. Moreover, support for several initially not supported programming features has been added (including, e.g., the possibility of analysing C++ and Java programs or support for re-entrant locks or lock guards). Through a number of experiments (including experiments with real-life code and real-life bugs), it is shown that the new version of Atomer is indeed much more general, scalable, and precise.
|
|
|
Kořeny moravské urbanistické struktury
Mohelník, Ladislav ; Löw, Jiří (oponent) ; Prokeš, Oldřich (oponent) ; Hrabec, Josef (oponent) ; Koutný, Jan (vedoucí práce)
Studium architektonických a urbanistických konceptů i jejich aplikaci v praxi, s ohledem na jejich historický kontext, je předmětem dalšího zájmu. Jde přitom především o odvěkou snahu člověka dosáhnout harmonického stavu v uspořádání světa okolo sebe, promítající se bezděčně do jeho díla. Cestami směřujícími k dosažení harmonie se v širším rámci teorie architektury a urbanismu zabývá architektonická kompozice, hledající vyváženost ve vztahu mezi formou, strukturou a prostorem jedinečného díla. Dílo založené na takovýchto hodnotách má zcela specifickou a současně přirozenou schopnost vypovídat o společenských podmínkách, jež provázely jeho vznik. Není v lidských sílách uchopit problematiku urbanistické struktury Moravy v celé její složitosti. Práce se proto soustřeďuje na dva klíčové sídelní prvky moravské urbanistické struktury, s ústřední rolí. Obec Ostravice je dnes poměrně malým sídlem v Moravskoslezských Beskydech, ale relikty její starobylosti vypovídají o významné minulosti, kdy se například v její plužině uchovaly kompoziční vztahy středověkého Civitas Dei převrstvující dokonce ještě starší sídelní jádro velkomoravského Děvína a Vogastisburgu. Listinně doložené děje a události vzdálené minulosti jsou ověřitelné pro danou lokalitu jejich prostorovou interpretaci v souvislostech širšího okolí Beskyd. Zánik sídla známého v poslední fázi jako tzv. Bruneswerde, neboli Brněnský hrad je ve 13. stol. provázen přenosem tradice do nového Brna, i s některými aspekty kompozičního uspořádání hlavních městských dominant. V urbanistické struktuře Moravy představuje toto bývalé hlavní město země logické pokračování role jejího dávného ústředí. Civitas Dei - boží Jeruzalém v opisu Augustinovy knihy De Civitate Dei, není jen oslavou Boha a náboženskou fantazií. Je také jedním z důležitých klíčů k poznání historické architektury. Vyobrazení "neznámého" sídla z knihy "neznámého" původu je skutečným skvostem vypovídajícím i o zaniklých architektonických dílech, dodnes zobrazených také ve vlastnických vztazích katastrálních map. Brněnský hrad, pramenný zdroj vznešenosti a síly, chránil, jak vyplývá z vyobrazení, ve svých zdech i sv. Vojtěcha, sv. Prokopa, sv. Václava a sv. Ludmilu. Vzhledem k bezprostřednímu lennímu vztahu k městu jsou tito BOE_MIENSES, bojovníci_půlměsíce, zasvěcenci Panny Marie a řádu sv. Jana Jeruzalémského, vyobrazeni v panenském městě bez aury. Tři hlavní chrámy, tři kompoziční osy symbolizované trojvěžím, jsou v analogickém vztahu k Brněnskému trojúhelníku čtyř svatých, Svaté rodině brněnského kostela. Staleté mocenské ambice představitelů města Brna a jeho duchovních řádů jsou vepsány do urbanistické struktury v podobě kompozičních vztahů srozumitelných jen těm, kdo jsou do tajemství jeho harmonie zasvěceni. Geometrický řád Brna je určen řadou zásad a kompozičních vztahů mezi prvky proměňujícími se v čase. Renesance nejenže potvrdila kvalitu středověkého založení města, ale současně ji vysoce sofistikovaným způsobem rozvinula a umožnila i relativně bezkolizní rozvoj za jeho hradbami až do poloviny 20. století. Naše současnost bohužel tyto kvality zcela přehlíží. Studium okolností, jež vedly ke vzniku rozsáhlých a složitých kompozic a vztahů, dává logiku jejich existenci skrze identifikaci a poznání osudů jejich tvůrců, uživatelů i majitelů. V souvislosti s Ostravicí i Brnem se tímto postupem lze nově dobrat mimořádně zajímavých osobností, umožňujících vnímat i starší poznatky v jiném světle.
|
|
|
Pokročilá statická analýza výkonnosti v nástroji Meta Infer
Pavela, Ondřej ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
Looper is a static complexity analysis tool for inference of tight upper bounds on the exe- cution cost of programs. It is based on the previously existing Loopus tool which used abstract program model of difference constraints (inequalities of the form + ), which allows for natural abstraction of common loop counter updates = + + and = + 0. Looper was initially proposed and implemented in author’s bachelor’s thesis as a checker for the Meta Infer framework but the tool failed to meet the expectations when tested on real-world code. This master’s thesis proposes a new improved version of Looper that aims at solving the main limitations of the original tool, namely through introduction of interprocedural analysis. Additionally, various extensions target- ing improved precision of the intraprocedural analysis, such as new abstraction algorithm, handling of compound loop conditions and more, were implemented. Moreover, logging, issue reporting and collection of results has been significantly improved. Finally, through extensive experiments with the new Looper version, the ability to analyze real-world code in a more general, scalable and precise way was shown.
|
|
|
Advanced Static Analysis of Atomicity in Concurrent Programs through Facebook Infer
Harmim, Dominik ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
Atomer is a static analyser based on the idea that if some sequences of functions of a multi-threaded program are executed under locks in some runs, likely, they are always intended to execute atomically. Atomer thus strives to look for such sequences and then detects for which of them the atomicity may be broken in some other program runs. The author of this master's thesis proposed and implemented the first version of Atomer as a plugin of the Facebook Infer framework in his bachelor's thesis. In the master's thesis, a new and significantly improved version of Atomer is proposed. The improvements aim at both increasing scalability as well as precision. Moreover, support for several initially not supported programming features has been added (including, e.g., the possibility of analysing C++ and Java programs or support for re-entrant locks or lock guards). Through a number of experiments (including experiments with real-life code and real-life bugs), it is shown that the new version of Atomer is indeed much more general, scalable, and precise.
|
|
|
Statická analýza v nástroji Facebook Infer zaměřená na detekci porušení atomičnosti
Harmim, Dominik ; Smrčka, Aleš (oponent) ; Vojnar, Tomáš (vedoucí práce)
Cílem této práce je navrhnout statický analyzátor, který bude sloužit pro detekci porušení atomicity. Navržený analyzátor Atomer je implementován jako modul pro Facebook Infer, což je volně šířený a snadno rozšířitelný nástroj, který umožňuje efektivní modulární a inkrementální analýzu. Analyzátor pracuje na úrovni sekvencí volání funkcí. Navržené řešení je založeno na předpokladu, že sekvence, které jsou zavolány atomicky jednou, by měly být pravděpodobně volány atomicky vždy. Implementovaný analyzátor byl úspěšně ověřen a vyhodnocen jak na malých programech, vytvořených pro testovací účely, tak na veřejně dostupných testovacích programech, které vznikly ze skutečných nízkoúrovňových programů.
|
|
|
Bedřich Kocek a česká novinářská fotografie
Sýkorová, Tereza ; Láb, Filip (vedoucí práce) ; Géla, František (oponent)
Diplomová práce Bedřich Kocek a česká novinářská fotografie se zabývá životem a tvorbou Bedřicha Kocka, fotoreportéra, který třicet let působil ve významném obrazovém týdeníku Svět v obrazech. Teoretická část specifikuje žánr novinářské fotografie a její vývoj od přelomu 19. a 20. století do 80. let 20. století. Na příkladu vývoje Světa v obrazech je nastíněn mediální a politický kontext v Československu od konce druhé světové války, kdy časopis vznikl, do 80. let, kdy Bedřich Kocek povolání fotoreportéra opustil. Důležitou částí práce je kapitola o životě Bedřicha Kocka, jenž dosud nebyl podrobněji popsán, která byla zpracována na základě osobních rozhovorů s fotografem za použití metody orální historie. Pomocí kompoziční analýzy práce zkoumá fotografické dílo Bedřicha Kocka a zjišťuje společné znaky jeho snímků, které byly součástí reportáží tvořených pro Svět v obrazech.
|
|
|
Kořeny moravské urbanistické struktury
Mohelník, Ladislav ; Löw, Jiří (oponent) ; Prokeš, Oldřich (oponent) ; Hrabec, Josef (oponent) ; Koutný, Jan (vedoucí práce)
Studium architektonických a urbanistických konceptů i jejich aplikaci v praxi, s ohledem na jejich historický kontext, je předmětem dalšího zájmu. Jde přitom především o odvěkou snahu člověka dosáhnout harmonického stavu v uspořádání světa okolo sebe, promítající se bezděčně do jeho díla. Cestami směřujícími k dosažení harmonie se v širším rámci teorie architektury a urbanismu zabývá architektonická kompozice, hledající vyváženost ve vztahu mezi formou, strukturou a prostorem jedinečného díla. Dílo založené na takovýchto hodnotách má zcela specifickou a současně přirozenou schopnost vypovídat o společenských podmínkách, jež provázely jeho vznik. Není v lidských sílách uchopit problematiku urbanistické struktury Moravy v celé její složitosti. Práce se proto soustřeďuje na dva klíčové sídelní prvky moravské urbanistické struktury, s ústřední rolí. Obec Ostravice je dnes poměrně malým sídlem v Moravskoslezských Beskydech, ale relikty její starobylosti vypovídají o významné minulosti, kdy se například v její plužině uchovaly kompoziční vztahy středověkého Civitas Dei převrstvující dokonce ještě starší sídelní jádro velkomoravského Děvína a Vogastisburgu. Listinně doložené děje a události vzdálené minulosti jsou ověřitelné pro danou lokalitu jejich prostorovou interpretaci v souvislostech širšího okolí Beskyd. Zánik sídla známého v poslední fázi jako tzv. Bruneswerde, neboli Brněnský hrad je ve 13. stol. provázen přenosem tradice do nového Brna, i s některými aspekty kompozičního uspořádání hlavních městských dominant. V urbanistické struktuře Moravy představuje toto bývalé hlavní město země logické pokračování role jejího dávného ústředí. Civitas Dei - boží Jeruzalém v opisu Augustinovy knihy De Civitate Dei, není jen oslavou Boha a náboženskou fantazií. Je také jedním z důležitých klíčů k poznání historické architektury. Vyobrazení "neznámého" sídla z knihy "neznámého" původu je skutečným skvostem vypovídajícím i o zaniklých architektonických dílech, dodnes zobrazených také ve vlastnických vztazích katastrálních map. Brněnský hrad, pramenný zdroj vznešenosti a síly, chránil, jak vyplývá z vyobrazení, ve svých zdech i sv. Vojtěcha, sv. Prokopa, sv. Václava a sv. Ludmilu. Vzhledem k bezprostřednímu lennímu vztahu k městu jsou tito BOE_MIENSES, bojovníci_půlměsíce, zasvěcenci Panny Marie a řádu sv. Jana Jeruzalémského, vyobrazeni v panenském městě bez aury. Tři hlavní chrámy, tři kompoziční osy symbolizované trojvěžím, jsou v analogickém vztahu k Brněnskému trojúhelníku čtyř svatých, Svaté rodině brněnského kostela. Staleté mocenské ambice představitelů města Brna a jeho duchovních řádů jsou vepsány do urbanistické struktury v podobě kompozičních vztahů srozumitelných jen těm, kdo jsou do tajemství jeho harmonie zasvěceni. Geometrický řád Brna je určen řadou zásad a kompozičních vztahů mezi prvky proměňujícími se v čase. Renesance nejenže potvrdila kvalitu středověkého založení města, ale současně ji vysoce sofistikovaným způsobem rozvinula a umožnila i relativně bezkolizní rozvoj za jeho hradbami až do poloviny 20. století. Naše současnost bohužel tyto kvality zcela přehlíží. Studium okolností, jež vedly ke vzniku rozsáhlých a složitých kompozic a vztahů, dává logiku jejich existenci skrze identifikaci a poznání osudů jejich tvůrců, uživatelů i majitelů. V souvislosti s Ostravicí i Brnem se tímto postupem lze nově dobrat mimořádně zajímavých osobností, umožňujících vnímat i starší poznatky v jiném světle.
|
|
| |
|
| |
host ::
RSS.